Nuprl Definition : ma-ef-val
11,40
postcript
pdf
M
.ef(
k
,
x
,
s
,
v
)?
w
== (
M
.2.2.2.2).1(<
k
,
x
>)?
s
,
v
.
w
(
s
,
v
)
latex
clarification:
M
.ef(
k
,
x
,
s
,
v
)?
w
== fpf-cap((
M
.2.2.2.2).1;product-deq(Knd;Id;KindDeq;IdDeq);<
k
,
x
>;
s
,
v
.
w
)(
s
,
v
)
latex
Definitions
f
(
a
)
,
f
(
x
)?
z
,
t
.1
,
t
.2
,
product-deq(
A
;
B
;
a
;
b
)
,
Knd
,
Id
,
KindDeq
,
IdDeq
,
<
a
,
b
>
,
x
.
A
(
x
)
FDL editor aliases
ma-ef-val
origin
s,v. w(s,v)
s,v. w)(s,v) s,v. w(s,v)
s,v. w)(s,v) x.A(x)